(declare-fun HTSab_new () Real)
(declare-fun ECxis_new () Real)
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun UAfuP_new () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(declare-fun Jlidu_new () Real)
(declare-fun x () Real)
(declare-fun e () Real)
(declare-fun ehbTa_new () Real)
(declare-fun f () Real)
(declare-fun y () Real)
(declare-fun CLPEA_new () Real)
(declare-fun g () Real)
(declare-fun h () Real)
(declare-fun i () Real)
(declare-fun j () Real)
(declare-fun t1428uscore0 () Real)
(declare-fun B () Real)
(declare-fun v2 () Real)
(declare-fun k () Real)
(declare-fun l () Real)
(declare-fun I2 () Real)
(declare-fun m () Real)
(declare-fun V () Real)
(declare-fun n () Real)
(declare-fun o () Real)
(declare-fun aa () Real)
(declare-fun z () Real)
(declare-fun A_shifted () Real)
(declare-fun p () Real)
(declare-fun q () Real)
(declare-fun r () Real)
(declare-fun v_shifted () Real)
(declare-fun s () Real)
(declare-fun t35uscore0dollarskuscore1_shifted () Real)
(declare-fun vuscore2dollarskuscore29_shifted () Real)
(declare-fun t () Real)
(declare-fun ab () Real)
(declare-fun u () Real)
(declare-fun ac () Real)
(assert (not (exists ((v Real)) (=> (xor (and (or (and (= j V (- f t)) (distinct (- y t) 0.0) (= (- y t) 2.0 (- d v_shifted)) (< (- (- x) (/ (* (- (- B))))) 0) (= (- Jlidu_new vuscore2dollarskuscore29_shifted) 2.0) (< (+ (/ v2)) (- ehbTa_new A_shifted)) (< 0.0 B)) (<= 0.0 (- HTSab_new (- b B)))) (<= (- HTSab_new (- 118 b B)) V) (<= 0.0 v2 V i) (< 0.0 V)) (< 0.0 (- CLPEA_new v_shifted))) (>= 0.0 (- a t)) (=> (xor (<= 0.0 v) (<= v (- a t))) (and (or (<= 0.0 j) (<= j V)) (<= 0.0 (+ (* (* (- 1.0) B) v) k) (+ (* (* (- 1.0) B) v) k) V) (<= (mod v 0.0) (- CLPEA_new v_shifted)))) (= (- ECxis_new) 2.0)))))
(assert (not (exists ((w Real)) (=> (and (or (and (xor (and (or (and (and (=> (>= 0.0 r (/ 164 UAfuP_new v2)) (and (and (<= 0.0 (+ (* r) I2)) (<= (+ (* A_shifted r) (- I2)) s)) (<= r (- f n)))) (< 0.0 (- UAfuP_new v2))) (distinct z ab) (= u 1.0)) (<= 0.0 (- Jlidu_new I2))) (<= (* 230 Jlidu_new I2) s) (< z ab) (= q 2.0) (< z ac) (< 0.0 (- HTSab_new g)) (<= 0.0 (- d l))) (<= (- 30 d l) s)) (<= 0.0 A_shifted)) (< 0.0 s)) (< 0.0 (- f n))) (> (+ (* A_shifted (- UAfuP_new v2)) (- Jlidu_new I2)) s)))))
(assert (= HTSab_new (+ g p)))
(assert (= ECxis_new (+ h)))
(assert (= a (+ t1428uscore0 t)))
(assert (= b (mod B p)))
(assert (= UAfuP_new (div v2 t35uscore0dollarskuscore1_shifted)))
(assert (distinct c (+ k A_shifted)))
(assert (= d (+ l v_shifted)))
(assert (= Jlidu_new (+ I2 vuscore2dollarskuscore29_shifted)))
(assert (distinct e (+ m t35uscore0dollarskuscore1_shifted)))
(assert (= f (+ n t)))
(assert (= y (div o t)))
(assert (= CLPEA_new (div aa v_shifted)))
(check-sat)
